c formula generated with seed 3, probabilty values 0.414000 0.028000 0.503000 and clause ration 4.410000
c the planted solution is {1, 2, 4, 6, 7, 8, 10, 11, 13, 17, 19, 20, 22, 23, 24, 25, 27, 29, 32, 33, 36, 42, 44, 47, 49, 51, 52, 53, 57, 59, 69, 79, 81, 82, 84, 86, 89, 92, 93, 94, 95, 96, 97, 98, 102, 104, 105, 107, 111, 113, 114, 118, 119, 125, 127, 129, 131, 132, 138, 140, 143, 145, 149, 151, 154, 155, 157, 158, 159, 161, 162, 165, 170, 174, 178, 180, 186, 187, 188, 189, 196, 197, 198, 199, 203, 204, 205, 207, 209, 211, 217, 218, 220, 222, 227, 229, 233, 236, 237, 238, 239, 241, 244, 245, 247, 250, 251, 255, 257, 258, 260, 262, 263, 268, 269, 270, 274, 276, 277, 279, 280, 283, 287, 291, 292, 294, 296, 298, 302, 303, 304, 306, 309, 311, 312, 313, 314, 317, 318, 320, 321, 322, 325, 327, 330, 331, 333, 336, 344, 348, 350, 351, 352, 353, 354, 356, 357, 363, 364, 369, 371, 374, 376, 385, 386, 388, 391, 399, 400}
p cnf 400 1764
-203 363 -77 0
81 -253 -375 0
220 134 240 0
-155 -278 -132 0
-257 -190 215 0
167 65 333 0
-308 -77 -96 0
98 -261 -252 0
-172 5 362 0
255 56 -26 0
301 -121 373 0
-96 331 221 0
-334 197 -271 0
-40 161 217 0
12 389 -14 0
-89 19 -149 0
-353 325 234 0
173 134 -379 0
-13 -206 168 0
-101 -97 147 0
-64 296 -112 0
-242 -115 306 0
-114 -98 -58 0
119 -358 -334 0
-186 -332 367 0
-230 -385 -131 0
272 210 -383 0
161 -230 306 0
221 -205 -75 0
360 155 -108 0
365 -248 137 0
-373 -57 -86 0
190 280 31 0
-253 -227 76 0
-247 378 -85 0
-199 49 224 0
271 -391 241 0
150 371 -196 0
364 90 136 0
-135 -257 -237 0
108 399 56 0
41 71 357 0
41 -306 105 0
-234 -178 153 0
224 54 -390 0
362 174 76 0
-250 -191 -44 0
61 -196 348 0
-233 -220 -297 0
-192 -33 -303 0
317 155 -58 0
151 -356 246 0
-28 -54 -208 0
385 -354 -143 0
124 70 -355 0
104 345 65 0
372 -202 246 0
-164 221 271 0
-147 -248 330 0
297 247 -245 0
-282 11 -103 0
370 9 -368 0
131 146 83 0
198 354 1 0
-240 130 -36 0
210 48 2 0
224 -44 -365 0
220 267 -158 0
311 -216 -381 0
95 -298 -203 0
-46 47 -83 0
19 127 400 0
298 -278 158 0
-6 -298 -230 0
132 66 282 0
213 324 51 0
-341 114 13 0
311 -137 -128 0
-278 295 -114 0
-310 -387 -108 0
163 -58 152 0
144 87 -310 0
348 -326 -60 0
323 -257 -46 0
41 220 -143 0
-231 75 -350 0
41 201 89 0
374 22 -112 0
-52 -239 245 0
247 318 -316 0
66 311 -218 0
-384 -46 237 0
203 -329 -324 0
-26 -274 134 0
-55 -227 14 0
-177 -148 309 0
85 -3 -292 0
231 267 211 0
-195 -374 17 0
261 -109 272 0
-115 -233 323 0
-106 93 11 0
-395 124 -27 0
287 -67 331 0
362 -293 76 0
-36 -104 -341 0
-224 185 337 0
248 204 164 0
58 137 353 0
-221 -200 -61 0
-138 -98 6 0
352 -296 -211 0
150 -101 -263 0
288 79 389 0
-100 307 182 0
12 -180 354 0
-208 -108 -394 0
-266 22 79 0
-30 -28 -271 0
-130 -323 157 0
-338 -335 -62 0
1 -189 -82 0
-117 -343 198 0
-274 -223 -388 0
57 -372 -221 0
-364 76 -168 0
-365 -269 295 0
146 180 89 0
229 -245 316 0
319 256 -120 0
-174 -299 228 0
11 260 -361 0
-210 311 391 0
-345 -158 355 0
84 5 240 0
211 231 301 0
-150 -27 88 0
380 12 -392 0
-150 113 -282 0
240 59 346 0
-253 -279 -262 0
128 -194 358 0
-383 204 -355 0
273 346 -267 0
74 258 -142 0
-198 177 -163 0
3 -143 19 0
-116 -74 -299 0
-359 -40 111 0
-276 -350 -14 0
-281 291 -307 0
306 57 81 0
-55 -358 -137 0
-237 -87 -262 0
-202 -26 337 0
86 3 -193 0
138 165 -367 0
15 -150 76 0
264 303 -174 0
-324 391 -194 0
57 -167 -28 0
58 -45 38 0
-322 -295 -257 0
-217 204 -157 0
-275 -358 207 0
-82 333 -161 0
266 -28 34 0
9 93 -237 0
85 121 154 0
-50 196 -55 0
150 -284 83 0
-322 330 -262 0
-294 298 175 0
-278 362 5 0
-80 -152 -389 0
279 -72 302 0
196 -397 -345 0
-127 396 -167 0
-258 370 399 0
58 -365 -374 0
-271 -175 -123 0
-264 382 361 0
390 326 197 0
-118 222 144 0
-39 24 241 0
-363 -273 -225 0
139 322 147 0
378 218 377 0
89 -342 -126 0
-141 196 -370 0
-388 150 320 0
203 -180 -42 0
-144 314 57 0
-336 -159 -389 0
27 68 278 0
-321 174 387 0
331 -229 31 0
-20 213 180 0
-17 -306 158 0
317 -117 -295 0
293 -361 299 0
163 289 255 0
-316 383 -91 0
278 -379 65 0
-48 157 348 0
17 -189 -292 0
126 1 -154 0
-61 -26 86 0
-321 178 11 0
-269 339 -21 0
-238 -51 -395 0
-70 142 335 0
-375 68 387 0
-21 42 -200 0
-306 174 193 0
47 274 -181 0
-382 -373 -77 0
-286 -132 100 0
-48 -98 236 0
-38 -187 183 0
274 179 -36 0
65 102 323 0
8 -367 330 0
88 -377 -239 0
-160 -358 105 0
-255 198 366 0
197 249 214 0
375 -244 25 0
-149 194 -136 0
268 309 -335 0
125 375 267 0
75 59 -158 0
-49 -48 46 0
-186 250 -230 0
-165 -7 -142 0
191 -113 138 0
111 110 139 0
246 283 -6 0
-117 288 -161 0
233 -35 -78 0
182 -395 -84 0
120 -14 226 0
-338 6 19 0
212 386 -81 0
-271 126 68 0
-198 -133 392 0
-398 -288 -359 0
-223 220 -378 0
122 -158 105 0
-177 43 -189 0
333 -250 -30 0
-219 -95 -29 0
95 337 398 0
86 -96 -154 0
-321 -158 331 0
41 382 -249 0
209 -230 47 0
-183 -172 259 0
-98 -159 196 0
136 135 227 0
324 275 -339 0
-128 -228 -326 0
174 212 -260 0
17 -390 96 0
355 249 251 0
-44 -207 138 0
266 123 270 0
-342 -169 -219 0
46 -186 204 0
-60 98 333 0
44 -125 -2 0
-20 -300 -158 0
387 208 -319 0
-30 2 -37 0
300 -238 -41 0
-248 325 -375 0
21 -110 -318 0
326 162 -257 0
-133 317 351 0
106 49 354 0
196 -83 280 0
-70 -344 354 0
22 -386 243 0
60 -306 -193 0
200 -236 151 0
-263 -360 301 0
206 -356 -264 0
-7 -335 -82 0
369 -295 -380 0
212 272 1 0
181 -127 69 0
-336 122 348 0
-360 -15 287 0
17 -241 120 0
-67 -261 -373 0
270 40 -11 0
-258 -371 -193 0
-158 207 -236 0
-106 279 -398 0
178 -338 -389 0
-188 -259 358 0
-2 -104 306 0
307 -255 -272 0
-83 -18 399 0
245 -262 242 0
-39 162 -48 0
-143 340 89 0
390 138 -345 0
-112 -99 79 0
105 -53 61 0
-312 -368 273 0
18 385 -283 0
158 -340 -173 0
-127 281 -172 0
-353 -329 -11 0
-322 16 -65 0
4 215 -178 0
-166 -191 140 0
-230 10 399 0
-6 277 121 0
112 214 250 0
-355 242 -309 0
-126 236 -324 0
-116 287 -254 0
199 -357 -140 0
103 -30 345 0
-38 350 95 0
234 -370 252 0
24 -198 -79 0
135 200 -106 0
-270 -5 368 0
-364 -43 -318 0
343 -218 157 0
-201 -37 351 0
-235 131 -246 0
291 -164 189 0
-191 -379 -347 0
-310 -54 270 0
-76 303 -343 0
-64 -106 -77 0
339 283 -96 0
341 99 -80 0
330 40 -307 0
294 358 225 0
-279 381 111 0
-135 137 377 0
-365 -353 150 0
299 -228 -189 0
-329 47 -133 0
269 -104 -309 0
-131 -281 230 0
263 81 -256 0
191 -44 294 0
-277 -204 -117 0
255 8 -379 0
327 -95 -151 0
70 -338 -27 0
44 -37 -308 0
299 114 -220 0
-386 -216 163 0
-339 -290 4 0
18 288 -308 0
261 103 -252 0
-163 369 205 0
177 -154 -284 0
291 128 77 0
336 -66 276 0
353 119 -265 0
-52 -325 -90 0
-78 88 -188 0
-166 -274 362 0
-159 -371 197 0
-128 303 276 0
-85 -266 262 0
-118 -89 24 0
-246 400 198 0
-157 -213 135 0
274 -206 95 0
-228 -300 -343 0
244 388 -106 0
-37 -56 -68 0
-328 -377 -221 0
-71 154 357 0
-65 127 -64 0
-106 -336 -163 0
164 119 77 0
154 262 -58 0
284 196 221 0
-72 333 51 0
111 187 -130 0
22 -101 6 0
-9 293 168 0
252 366 262 0
250 -269 -4 0
219 191 314 0
-313 -356 318 0
187 -144 -100 0
356 -26 -55 0
-74 271 137 0
-52 -380 -113 0
249 -218 -235 0
-257 270 -211 0
248 -131 -201 0
-115 -387 118 0
-239 265 174 0
81 204 1 0
161 -13 285 0
-139 94 53 0
301 -303 -264 0
167 -121 -165 0
64 -170 162 0
-107 85 -50 0
-250 -151 277 0
364 293 -158 0
-180 -250 317 0
-358 69 400 0
84 -218 175 0
-74 329 282 0
-266 -58 -381 0
-354 -218 -45 0
-280 214 180 0
-177 386 -64 0
-260 -272 -94 0
-363 -68 -274 0
266 -12 144 0
159 -253 -152 0
-288 357 250 0
-321 -361 -24 0
-65 -360 132 0
151 160 306 0
371 110 41 0
252 183 269 0
-358 400 -191 0
-232 -270 -13 0
-192 -373 -28 0
-86 -104 386 0
207 257 321 0
75 -103 171 0
-255 -368 109 0
-198 229 123 0
78 -301 -327 0
-49 120 -361 0
114 -304 378 0
-141 12 -245 0
-255 326 262 0
-350 81 335 0
-342 102 57 0
138 111 292 0
-218 377 2 0
-19 -374 -288 0
-380 -305 -38 0
25 59 239 0
368 242 -349 0
-266 -78 127 0
332 305 104 0
-115 -358 -267 0
-286 10 -200 0
-353 64 -332 0
127 -382 -248 0
348 309 -201 0
372 -187 98 0
227 -285 -15 0
-228 67 -24 0
79 146 77 0
-166 196 -219 0
227 73 -205 0
106 68 145 0
-79 73 -370 0
-196 -103 99 0
371 184 243 0
115 -198 258 0
-261 153 -199 0
116 -334 243 0
298 -86 67 0
159 -175 59 0
-187 -273 -320 0
-26 88 -145 0
-263 -102 -146 0
-250 185 -128 0
100 141 236 0
-100 47 -307 0
47 129 -393 0
-358 -221 -45 0
-48 -357 307 0
36 -266 57 0
-341 304 -16 0
-372 -91 363 0
-34 162 317 0
-204 56 -193 0
-34 -234 -184 0
-101 331 304 0
-392 128 -298 0
208 343 -171 0
304 -39 -231 0
-357 -285 -129 0
251 -158 -399 0
374 -150 187 0
-163 -274 144 0
-130 298 -193 0
-102 -38 307 0
317 51 262 0
-160 -164 113 0
-202 263 119 0
187 -366 162 0
-213 -235 19 0
-357 171 82 0
170 239 -179 0
285 -72 190 0
-275 270 -346 0
-70 -229 29 0
-9 -306 -298 0
374 59 -179 0
-328 -208 187 0
-52 150 -299 0
-231 -395 106 0
156 315 111 0
-316 393 149 0
385 -329 -77 0
-119 161 324 0
-296 81 88 0
-389 243 213 0
-81 331 -207 0
74 -296 321 0
-185 217 -75 0
187 56 -7 0
179 -126 37 0
143 75 69 0
-29 138 35 0
376 104 24 0
-164 -102 346 0
-292 133 327 0
393 209 377 0
152 335 -137 0
-396 -184 23 0
49 -96 -245 0
90 187 191 0
-138 300 -213 0
193 -296 -176 0
48 312 74 0
272 -112 14 0
64 -331 -163 0
-111 -298 20 0
264 342 140 0
268 -59 277 0
-322 59 -369 0
-59 -366 -24 0
-41 -100 -225 0
399 -32 346 0
104 -8 101 0
213 103 -70 0
-353 -6 127 0
103 203 -269 0
243 -16 342 0
-355 -110 -392 0
-11 -377 183 0
389 91 151 0
-229 247 226 0
-150 139 345 0
19 391 -235 0
-400 288 -3 0
-50 -190 348 0
322 319 31 0
4 -97 -92 0
240 -392 -268 0
-146 218 274 0
-342 -381 198 0
-142 -126 304 0
103 137 82 0
-326 -57 -72 0
378 -299 137 0
-12 343 259 0
350 55 -209 0
-149 -11 -367 0
-223 -240 -294 0
62 363 26 0
243 124 -373 0
-359 290 150 0
-174 -378 -129 0
165 -397 -326 0
179 -118 33 0
61 192 -130 0
-59 168 -48 0
-28 -81 229 0
-251 -50 168 0
237 -88 36 0
-356 -262 29 0
-164 -9 165 0
-111 95 -203 0
-265 -89 343 0
-70 93 -347 0
52 -321 216 0
188 -121 217 0
-47 272 298 0
269 -353 -33 0
-304 297 -259 0
-146 -53 -280 0
140 -7 -95 0
26 -142 392 0
-398 -156 -115 0
-373 -228 -341 0
-221 333 -168 0
-309 -257 159 0
-147 55 139 0
-319 -247 -48 0
-381 121 208 0
126 -151 -28 0
106 -134 115 0
-77 -24 -165 0
-179 -387 -171 0
-75 -385 366 0
118 -150 7 0
-102 188 21 0
-117 126 -159 0
-185 51 33 0
137 133 205 0
-5 -263 -391 0
150 314 394 0
113 -178 60 0
184 295 241 0
159 75 329 0
194 -173 224 0
135 141 -191 0
-146 283 -395 0
196 -218 281 0
-200 176 -309 0
-145 -138 -235 0
-232 -281 -340 0
-306 -194 75 0
-73 34 -376 0
331 340 50 0
94 -129 -344 0
84 -54 186 0
177 92 -151 0
4 -211 -306 0
-386 133 -100 0
-349 195 316 0
-170 47 379 0
-222 186 213 0
-224 399 111 0
63 166 13 0
231 -242 -187 0
236 -331 -258 0
362 161 -155 0
139 359 -397 0
194 327 -270 0
-1 226 -346 0
-315 137 297 0
-93 -190 213 0
-393 261 290 0
-171 -179 -361 0
37 332 -9 0
275 -34 379 0
-236 -150 -57 0
168 -28 71 0
234 -147 369 0
20 59 -246 0
71 -206 -10 0
-352 242 -214 0
314 -135 273 0
-107 -154 276 0
-288 63 55 0
193 -157 -358 0
-262 -91 3 0
75 -247 -215 0
-358 384 -346 0
124 -210 192 0
-240 277 -65 0
248 253 -83 0
282 -170 -191 0
247 238 391 0
81 -218 -356 0
361 1 -386 0
-124 -374 232 0
-316 -20 208 0
298 37 288 0
258 227 -389 0
391 165 -301 0
185 -68 -82 0
359 306 62 0
306 -388 213 0
173 -99 -268 0
287 288 -237 0
254 263 300 0
-297 -131 310 0
-362 -147 241 0
-213 235 110 0
-317 50 -181 0
399 142 -218 0
42 -162 396 0
146 219 -337 0
-43 -107 160 0
307 266 129 0
-231 287 158 0
-260 -93 -100 0
285 180 -385 0
-146 -291 -89 0
-302 70 -173 0
136 -16 31 0
89 361 223 0
207 36 -66 0
-150 261 -188 0
350 -176 -85 0
244 287 232 0
-326 -16 8 0
341 -338 83 0
231 -197 352 0
-201 76 398 0
328 -65 266 0
-137 3 110 0
-396 -61 -146 0
-200 -123 -164 0
124 73 127 0
253 -219 352 0
352 -292 -188 0
244 86 -246 0
231 208 -166 0
85 18 -343 0
178 26 195 0
-389 -120 352 0
356 10 -135 0
-127 5 298 0
3 -16 -304 0
-179 134 -304 0
156 52 66 0
-344 -54 323 0
-390 -26 197 0
243 -315 -159 0
231 -176 373 0
224 186 -97 0
-229 180 75 0
148 399 -187 0
-91 398 -6 0
192 395 -242 0
64 -367 249 0
-180 126 97 0
124 330 87 0
-231 -317 232 0
323 -301 -298 0
340 -375 334 0
-377 245 218 0
-231 62 265 0
-59 -287 302 0
-150 3 116 0
-113 -156 -349 0
-380 -49 -236 0
93 -286 51 0
-20 -95 -373 0
-164 -70 180 0
149 -308 -212 0
201 85 374 0
-15 74 -276 0
290 118 267 0
354 -328 -300 0
-199 214 274 0
-155 46 29 0
-76 334 231 0
-248 314 -37 0
139 -371 -120 0
-84 -275 -283 0
320 -310 111 0
322 30 -268 0
173 155 101 0
151 -322 55 0
-173 211 -339 0
246 239 -17 0
174 -190 81 0
-123 218 -359 0
-37 -94 -229 0
47 195 324 0
-200 212 397 0
-375 -382 -106 0
-38 -252 -35 0
-63 193 90 0
-86 -37 -170 0
28 -171 380 0
81 122 58 0
360 -269 145 0
115 -362 -149 0
194 -346 83 0
-106 -324 -393 0
-150 -364 -19 0
357 -15 -243 0
363 262 36 0
-238 99 -76 0
336 -52 379 0
-64 235 -250 0
-293 -97 -159 0
156 95 -276 0
-13 135 -378 0
-77 -28 158 0
119 336 -224 0
239 348 -265 0
189 -305 261 0
166 135 270 0
170 302 277 0
87 131 -234 0
328 206 -223 0
-194 247 238 0
-48 150 213 0
70 158 397 0
-135 362 51 0
8 103 248 0
-120 -360 -347 0
47 180 203 0
137 -233 -61 0
56 -72 -399 0
-109 292 -282 0
282 112 165 0
118 -152 363 0
-135 -50 -299 0
-226 384 -399 0
-362 -379 360 0
219 117 -112 0
-161 -295 370 0
-168 -21 -116 0
306 -269 328 0
-56 348 -160 0
172 162 78 0
96 -380 119 0
-163 166 -332 0
372 -115 28 0
52 69 245 0
-62 126 11 0
-237 141 -87 0
382 77 -372 0
124 -378 -317 0
298 -58 -112 0
-355 31 122 0
-36 238 183 0
390 -77 -47 0
-46 303 53 0
-216 13 -164 0
227 206 -259 0
-164 42 29 0
-146 -52 -260 0
254 325 160 0
84 -100 371 0
-2 104 -187 0
-254 -391 -7 0
286 242 -112 0
-59 184 -248 0
-198 153 162 0
-367 101 225 0
-255 -59 -166 0
108 65 -319 0
-312 274 -207 0
-249 -290 -343 0
240 -306 52 0
-128 9 -103 0
378 -4 322 0
-370 -359 -202 0
364 207 -31 0
143 -14 -319 0
347 -321 -395 0
248 -150 343 0
-372 -268 156 0
-54 -131 324 0
-34 -375 -362 0
122 2 272 0
339 298 126 0
-296 315 44 0
-262 -358 190 0
-232 -195 69 0
177 211 112 0
300 155 370 0
274 2 -166 0
175 185 353 0
18 -172 115 0
384 -98 354 0
-357 -180 157 0
362 -348 399 0
-344 225 -9 0
80 181 348 0
379 -241 -75 0
-55 -155 200 0
-83 7 -341 0
159 -379 237 0
-396 -144 113 0
151 -331 -44 0
30 -188 291 0
65 32 31 0
-391 14 320 0
-326 -384 93 0
29 -399 88 0
34 49 -376 0
-30 73 -344 0
112 -321 -12 0
-320 265 22 0
-382 -93 -268 0
35 -201 -364 0
254 157 -149 0
-274 -242 -91 0
85 400 -311 0
46 352 -320 0
337 -325 -75 0
-339 -310 -392 0
60 -306 -168 0
-89 -113 84 0
192 174 -302 0
139 -155 52 0
-47 -145 -290 0
327 336 -301 0
-55 9 267 0
263 -248 149 0
104 -225 -212 0
53 336 -63 0
382 -379 254 0
21 -143 -62 0
-358 278 -33 0
-20 347 59 0
-132 388 243 0
244 32 -345 0
199 -204 160 0
-333 -100 -165 0
-20 -393 -7 0
-87 -144 10 0
254 216 -99 0
158 -290 -65 0
-396 -119 72 0
-53 -187 138 0
230 -28 152 0
-150 201 -94 0
375 14 -389 0
-41 32 255 0
-249 -173 -106 0
-176 -179 -50 0
206 11 362 0
-11 -203 250 0
88 12 7 0
-257 276 -287 0
151 263 -101 0
-328 55 286 0
293 -241 298 0
-249 -220 56 0
-312 11 109 0
-145 -112 -36 0
5 203 393 0
279 -194 -80 0
-205 -183 -20 0
221 367 -243 0
-146 -213 -345 0
1 -334 283 0
-81 -143 207 0
145 325 170 0
-256 -235 -323 0
-94 -221 121 0
6 66 146 0
-339 -124 -301 0
230 354 379 0
-310 251 -300 0
344 230 383 0
-310 185 48 0
-325 -323 60 0
61 -334 -19 0
375 370 -206 0
255 299 361 0
60 -299 397 0
-359 -230 -392 0
52 242 135 0
204 -372 263 0
-373 -63 -118 0
-320 -377 -205 0
111 170 186 0
-118 -109 -274 0
354 304 -326 0
249 -301 345 0
342 50 -326 0
-212 228 206 0
-328 -138 187 0
158 190 -290 0
39 178 171 0
-187 367 -171 0
-375 -230 -121 0
-163 -167 -200 0
-109 339 368 0
323 136 102 0
336 -384 -297 0
385 -37 -164 0
182 369 -322 0
-282 96 54 0
250 209 277 0
-79 -208 62 0
-340 -254 313 0
-56 -315 -153 0
-339 220 -21 0
301 114 -330 0
145 250 -373 0
14 307 49 0
185 -308 293 0
-46 -325 -227 0
192 97 172 0
311 -219 -267 0
-374 116 -297 0
302 102 -137 0
-43 -264 27 0
-66 -187 -296 0
-103 -392 274 0
142 -71 -391 0
-359 367 -327 0
112 384 -14 0
330 385 -254 0
-286 -147 298 0
-252 -384 -91 0
-257 123 -12 0
-249 -100 331 0
-31 358 -113 0
218 312 -285 0
-175 -156 9 0
-378 253 282 0
-229 108 333 0
-165 -294 -366 0
138 -141 -153 0
-398 237 -267 0
-156 -75 351 0
-8 357 -269 0
97 292 -200 0
-319 -399 190 0
166 12 251 0
344 -380 386 0
215 -394 -86 0
-200 -199 -159 0
107 239 -382 0
-28 400 1 0
131 -173 -377 0
-65 71 83 0
310 -211 -248 0
-371 292 275 0
269 196 -40 0
12 -219 -182 0
267 -72 -69 0
-82 149 54 0
-292 100 102 0
-13 307 -54 0
-344 56 -150 0
-22 -360 319 0
-384 221 -282 0
55 -233 217 0
-136 250 -362 0
381 -141 -2 0
387 338 -134 0
-272 -43 186 0
-264 263 -175 0
-327 -270 -232 0
-50 199 -99 0
-301 240 46 0
137 210 -38 0
-332 140 -315 0
265 282 -328 0
234 163 19 0
85 -266 -294 0
-196 -290 -25 0
339 -85 252 0
375 257 228 0
264 276 3 0
256 175 276 0
-275 177 -196 0
96 -335 -198 0
-387 -251 -279 0
133 400 -158 0
192 -376 119 0
-104 350 373 0
205 182 358 0
194 150 19 0
225 -341 -53 0
-140 -343 153 0
41 201 187 0
-311 338 317 0
92 135 -250 0
-148 328 214 0
-187 -182 -98 0
-49 189 56 0
-211 -66 324 0
-296 298 -250 0
-9 -66 400 0
-10 -389 -159 0
-192 277 -48 0
331 19 -76 0
75 -347 -155 0
129 358 -104 0
-253 140 -192 0
47 -211 226 0
127 -89 172 0
-100 -193 -130 0
122 141 47 0
-253 316 -269 0
-275 99 366 0
82 84 364 0
98 13 -379 0
295 -319 -27 0
-248 119 -360 0
-16 125 -393 0
137 -306 -259 0
99 -363 -202 0
270 -4 -69 0
372 202 363 0
368 101 -15 0
41 -44 -293 0
356 76 254 0
-278 171 152 0
-224 -61 3 0
-247 -159 69 0
143 -399 -197 0
134 199 378 0
185 375 81 0
-91 247 -182 0
-238 -373 -399 0
45 -385 351 0
388 -301 186 0
-379 230 392 0
126 -141 288 0
30 323 47 0
-209 -35 -312 0
-109 -69 -32 0
-185 -268 383 0
236 206 393 0
-232 -272 -366 0
73 8 -203 0
-52 95 275 0
119 -274 146 0
361 -13 245 0
147 -80 141 0
175 -29 -177 0
-137 -236 54 0
385 -62 -76 0
-340 -291 160 0
182 -74 41 0
-6 -385 170 0
-386 -250 -28 0
35 -6 92 0
247 231 -6 0
118 -15 -48 0
-302 122 178 0
250 -211 -257 0
38 390 -307 0
-113 217 116 0
-219 -256 -185 0
-277 -347 -19 0
-247 9 211 0
395 -126 -330 0
196 -240 348 0
-234 56 335 0
-175 -45 -324 0
-176 -183 -133 0
-323 162 -122 0
371 137 41 0
396 250 -260 0
350 -43 -379 0
353 392 -322 0
-343 -155 -138 0
368 -213 281 0
51 151 -128 0
-117 -365 -290 0
-142 -205 226 0
-192 250 -271 0
113 -203 -309 0
111 293 194 0
243 118 214 0
269 186 -285 0
-368 17 -275 0
-349 -51 -42 0
-152 351 -35 0
-359 -221 -289 0
128 49 206 0
-211 88 357 0
150 -204 -359 0
-351 167 42 0
-194 -217 281 0
-199 91 325 0
-34 6 236 0
197 284 319 0
-176 158 180 0
194 -396 55 0
-222 391 61 0
-134 111 -74 0
-319 -75 79 0
342 367 -46 0
296 84 140 0
366 -205 -365 0
-254 131 211 0
259 321 -313 0
-74 -255 334 0
-316 -71 331 0
-134 20 -152 0
383 -303 -288 0
-304 -112 88 0
373 214 -273 0
-306 134 162 0
38 -22 227 0
173 -275 83 0
174 -99 52 0
-137 120 -155 0
138 -242 -172 0
-300 -32 -57 0
-91 -109 -275 0
-272 24 82 0
-118 67 -349 0
384 394 -343 0
362 -391 119 0
150 -277 -341 0
-41 14 -121 0
-329 -41 189 0
76 400 208 0
282 126 -256 0
-48 47 -141 0
-48 338 -386 0
4 -196 -258 0
-315 -152 -355 0
264 297 -266 0
137 360 -368 0
273 -23 209 0
155 -332 49 0
-193 92 311 0
-7 128 -73 0
81 296 -103 0
316 385 -105 0
159 297 133 0
85 12 306 0
301 -342 -93 0
-242 -179 -299 0
-111 -268 -310 0
-10 -250 -16 0
209 98 102 0
272 -233 113 0
-367 183 221 0
-339 -161 157 0
89 -175 321 0
-193 -78 -201 0
120 33 264 0
-169 19 -71 0
354 -66 250 0
-30 -142 -174 0
-239 -132 94 0
67 -79 -101 0
137 353 -333 0
94 -46 302 0
197 -299 -390 0
278 113 354 0
-273 -206 -140 0
-202 302 314 0
-371 124 -232 0
369 253 164 0
-44 -234 185 0
3 179 229 0
216 274 79 0
-353 196 76 0
325 -72 -167 0
-105 263 -32 0
-353 2 393 0
-100 -390 -191 0
366 354 -151 0
148 149 176 0
-345 -108 -64 0
-231 -306 213 0
-44 -75 335 0
-148 171 282 0
235 -106 77 0
-131 -161 -345 0
-398 94 386 0
382 -37 121 0
-72 173 -124 0
-181 49 -35 0
-63 -121 8 0
-15 -135 -46 0
127 -286 -347 0
361 58 -100 0
351 -188 149 0
14 -288 75 0
201 -277 348 0
-140 -14 282 0
69 -46 158 0
4 -294 -237 0
-365 94 207 0
-309 -277 -221 0
-361 36 292 0
130 -127 -271 0
261 -1 -338 0
-341 -192 -141 0
-100 116 212 0
-298 -361 -102 0
-217 64 -190 0
115 85 -335 0
-46 -209 -113 0
39 117 -14 0
264 216 -90 0
-373 393 -399 0
-305 349 -149 0
47 -96 14 0
-123 353 376 0
367 136 -305 0
393 -223 -374 0
-257 334 279 0
311 122 -236 0
-144 372 9 0
-70 380 254 0
351 -219 159 0
-400 -166 136 0
-70 119 77 0
220 241 -299 0
-400 143 -353 0
-345 251 260 0
-166 -31 -117 0
258 -198 194 0
-301 -204 21 0
-22 308 -389 0
-197 400 -287 0
-386 -308 134 0
158 -135 -37 0
320 -268 35 0
350 -113 -27 0
98 -138 259 0
116 142 149 0
363 -1 -279 0
-276 134 327 0
78 -399 165 0
-134 -101 -347 0
218 127 -252 0
116 260 -125 0
-372 -298 146 0
348 -143 -7 0
-125 320 -151 0
-143 -229 233 0
113 -330 -59 0
210 218 395 0
385 -172 -48 0
117 -309 -128 0
-144 286 167 0
330 352 254 0
-60 -288 -34 0
87 346 93 0
-320 -59 304 0
329 373 -39 0
399 -105 341 0
-1 -85 -93 0
392 -372 384 0
246 390 -166 0
-356 314 26 0
32 138 303 0
347 -67 99 0
294 -319 236 0
59 307 -114 0
325 258 314 0
-248 -78 283 0
-352 -192 380 0
333 361 67 0
-133 334 362 0
-168 -184 -254 0
-314 169 -195 0
-275 -243 10 0
-14 -88 388 0
-287 -317 369 0
299 -38 398 0
315 -307 108 0
163 -362 373 0
332 -276 -378 0
-281 -120 -152 0
-310 390 -143 0
1 -17 126 0
67 -256 -262 0
67 373 -163 0
-187 115 -166 0
185 391 100 0
-28 145 157 0
-74 25 143 0
305 301 140 0
156 -93 -225 0
296 344 327 0
86 74 62 0
208 -281 -227 0
29 -246 -90 0
88 23 -222 0
-321 182 -261 0
14 -44 -60 0
142 279 281 0
221 282 8 0
-131 -281 71 0
-93 -199 -28 0
-268 14 -191 0
249 -203 245 0
-168 17 -301 0
-126 76 -271 0
-202 326 243 0
-312 -384 271 0
-268 -26 359 0
300 -197 351 0
288 293 385 0
-127 -211 -282 0
-151 -398 305 0
-145 -16 -105 0
223 206 386 0
-53 -103 -86 0
-198 -143 369 0
161 -40 -312 0
-47 -364 -224 0
324 -395 -189 0
110 229 361 0
-272 263 -31 0
-48 -293 7 0
-380 199 -71 0
-362 -324 269 0
294 -6 -42 0
-241 257 -258 0
-175 -181 93 0
-195 -141 227 0
325 -261 98 0
-382 264 366 0
-159 -203 227 0
273 -354 -375 0
20 -12 -90 0
12 -210 -294 0
-350 -57 -56 0
-58 345 267 0
-45 -31 -230 0
264 -364 -136 0
140 372 -296 0
-349 -326 204 0
-263 -237 -103 0
269 -359 385 0
-109 22 -248 0
-216 229 -335 0
97 137 340 0
-246 -113 -376 0
-307 -21 209 0
-205 -370 383 0
-181 -348 139 0
-142 -350 295 0
-37 -342 189 0
-231 323 -149 0
-328 357 -381 0
-189 10 345 0
270 -200 -48 0
-86 -269 -337 0
208 -294 93 0
269 -34 -201 0
-321 123 357 0
-361 -192 -77 0
336 -84 -229 0
-279 80 237 0
-165 147 312 0
-181 -28 245 0
332 97 76 0
-18 141 50 0
275 -294 140 0
-50 -85 327 0
41 -31 -292 0
-225 136 -138 0
295 -130 -218 0
328 145 -388 0
187 -21 -115 0
-320 -72 224 0
-265 -349 -100 0
-196 289 -332 0
193 -89 -74 0
-68 264 -388 0
22 -12 -40 0
-33 -310 -43 0
-318 -242 130 0
-181 -252 399 0
-100 299 375 0
194 -15 396 0
190 -37 -159 0
72 -70 394 0
-230 -366 -99 0
226 234 145 0
301 -68 148 0
193 369 381 0
-68 30 -257 0
-346 202 -364 0
-27 -227 -168 0
68 -187 -185 0
392 151 -251 0
105 -374 273 0
-285 324 -262 0
-287 -189 79 0
377 -363 86 0
174 388 348 0
-296 125 -32 0
-182 358 265 0
400 -177 -3 0
-101 -113 365 0
-119 256 143 0
-124 338 -318 0
231 382 11 0
37 -142 -277 0
-264 263 236 0
344 -136 159 0
85 -54 -98 0
126 382 -379 0
82 166 -189 0
128 -310 360 0
392 -265 -311 0
363 -265 -305 0
81 233 237 0
-98 26 276 0
-285 314 -124 0
-122 -185 143 0
-331 1 334 0
332 199 297 0
-21 343 -127 0
10 251 270 0
296 -313 266 0
-152 84 -171 0
-129 230 -389 0
118 -256 -156 0
371 -384 -226 0
-332 -389 44 0
-32 -350 217 0
-66 -397 -206 0
-66 -192 129 0
-187 -213 -157 0
370 -92 -324 0
15 -305 108 0
-78 325 20 0
12 168 13 0
99 173 263 0
59 -131 286 0
-13 329 -70 0
87 334 197 0
199 370 -257 0
230 40 -288 0
-76 343 58 0
170 -396 -168 0
-196 -288 -11 0
290 232 -120 0
240 400 12 0
-123 238 -117 0
-358 242 226 0
330 121 -320 0
-371 352 -344 0
-282 180 -228 0
-354 391 63 0
-338 279 59 0
-42 308 -183 0
-384 60 141 0
145 -374 141 0
-256 364 107 0
201 337 57 0
-259 -47 -105 0
394 118 -359 0
75 -207 317 0
-141 355 -369 0
-176 -107 279 0
196 6 -367 0
238 -324 -232 0
120 -259 397 0
-121 163 -67 0
369 -326 17 0
207 -28 -288 0
-38 -70 -383 0
150 -349 -205 0
169 -174 -297 0
386 -322 -102 0
-179 208 26 0
132 119 277 0
-90 162 64 0
329 220 83 0
-170 5 238 0
-70 104 -334 0
7 374 25 0
354 -271 331 0
-88 -281 257 0
-347 -176 -355 0
214 73 218 0
-28 -276 -162 0
368 38 -91 0
48 -315 -155 0
217 141 243 0
-379 302 131 0
-77 -136 241 0
-252 -349 312 0
-92 313 -145 0
187 -85 -126 0
-140 87 59 0
143 -156 -206 0
-101 -284 -106 0
394 318 41 0
-40 33 138 0
-185 357 8 0
-324 -357 -95 0
332 319 363 0
-62 -68 391 0
-37 169 -180 0
51 -159 -19 0
233 -222 -42 0
305 3 -393 0
-18 -321 -353 0
139 335 8 0
-48 337 103 0
291 -396 238 0
-216 223 109 0
165 167 -158 0
212 85 -310 0
-46 -116 222 0
266 -392 137 0
-351 337 -34 0
33 164 -24 0
-104 304 141 0
-104 311 80 0
-70 386 199 0
83 -166 142 0
143 -279 -312 0
-295 -301 158 0
167 -295 184 0
-46 -12 247 0
357 163 192 0
87 342 -41 0
35 -219 167 0
-250 267 -106 0
255 31 71 0
27 -322 265 0
304 216 167 0
-358 79 371 0
384 367 -26 0
376 -326 -393 0
379 262 -353 0
143 18 195 0
-25 -27 119 0
-374 29 90 0
-192 372 -24 0
294 241 -310 0
-230 222 274 0
-65 -217 15 0
261 -191 169 0
220 -318 347 0
259 -88 226 0
181 -380 -322 0
-219 -362 199 0
244 268 -282 0
351 -370 -219 0
-264 -155 -44 0
289 158 -205 0
-293 364 -242 0
-240 -224 351 0
-139 320 -175 0
-218 -203 -345 0
310 205 345 0
-248 104 187 0
155 321 25 0
332 -161 -334 0
-147 59 241 0
87 173 -177 0
27 302 -166 0
-20 347 -91 0
-215 66 -134 0
140 270 287 0
-4 23 45 0
360 -78 -94 0
207 -77 199 0
-65 312 270 0
-196 365 325 0
-33 -394 249 0
95 393 193 0
-342 251 -326 0
362 42 -167 0
203 -152 -176 0
-394 -52 -314 0
50 -36 258 0
-100 162 -76 0
301 -83 375 0
-359 267 362 0
198 358 173 0
-176 -10 88 0
-193 352 274 0
112 388 299 0
-66 18 150 0
311 351 -355 0
375 -157 -78 0
207 325 -341 0
50 155 191 0
-222 29 230 0
100 233 -353 0
-292 268 58 0
237 15 87 0
50 -144 266 0
88 -26 201 0
-97 -346 -32 0
-45 154 -121 0
373 -285 173 0
50 246 69 0
-11 351 -125 0
24 161 336 0
-24 296 -186 0
-253 105 -324 0
-349 -58 -225 0
134 53 -100 0
-173 95 -288 0
-196 241 -324 0
217 -123 320 0
-75 379 160 0
29 -165 137 0
-90 235 -333 0
370 359 -261 0
-265 -78 -88 0
302 333 154 0
-46 11 -171 0
-150 362 230 0
-289 227 188 0
-90 -138 186 0
165 161 298 0
45 14 -177 0
21 168 -182 0
163 -264 15 0
397 -244 -380 0
-50 83 139 0
-320 236 -189 0
9 -388 -290 0
275 -253 147 0
-231 60 -279 0
307 365 260 0
311 -51 -172 0
-146 -359 -240 0
58 47 78 0
-399 150 -176 0
-134 302 -110 0
187 -146 -249 0
318 39 -257 0
21 11 -276 0
398 -233 -191 0
314 -304 -105 0
-131 277 108 0
-293 -103 -359 0
184 70 92 0
-135 -371 -306 0
-259 -171 8 0
91 154 191 0
179 61 -289 0
-135 -327 26 0
219 -67 106 0
-208 -104 346 0
-334 243 103 0
-373 270 -158 0
-74 -240 -129 0
-288 123 -217 0
293 209 108 0
200 -102 371 0
-42 204 395 0
-362 -231 237 0
151 307 230 0
337 52 -351 0
306 -233 380 0
66 328 -289 0
-360 231 -111 0
-324 -217 -221 0
-204 -196 -235 0
382 -186 364 0
179 47 -189 0
74 -348 57 0
31 -195 -205 0
-31 -16 -156 0
13 -194 -273 0
162 -205 -154 0
257 -37 -375 0
112 355 -139 0
267 -361 289 0
-116 -301 -211 0
-378 -161 66 0
-247 307 352 0
56 -237 -83 0
307 138 383 0
-42 -164 -125 0
-366 -120 354 0
194 -293 -229 0
154 -3 158 0
195 146 24 0
-254 -304 396 0